﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Aima.Core.Logic.Propositional.Algorithms
{
    using System.Collections;

    using Aima.Core.Logic.Propositional.Parsing;
    using Aima.Core.Logic.Propositional.Parsing.AST;
    using Aima.Core.Logic.Propositional.Visitors;
    using Aima.Core.Util;

    public class WalkSAT
    {
        private Model myModel;

        private Random random = new Random();

        public Model FindModelFor(String logicalSentence, int numberOfFlips,
                double probabilityOfRandomWalk)
        {
            this.myModel = new Model();
            var s = (Sentence)new PEParser().Parse(logicalSentence);
            var transformer = new CNFTransformer();
            var clauseGatherer = new CNFClauseGatherer();
            var sc = new SymbolCollector();

            var symbols = sc.GetSymbolsIn(s).ToList();
            var r = new Random();
            foreach (var sym in symbols)
            {
                this.myModel = this.myModel.Extend(sym, Util.RandomBoolean());
            }

            IList<Sentence> clauses = clauseGatherer.GetClausesFrom(transformer.Transform(s)).ToList(); 

            for (int i = 0; i < numberOfFlips; i++)
            {
                if (this.GetNumberOfClausesSatisfiedIn(new Converter<Sentence>()
                        .ListToSet(clauses), myModel) == clauses.Count)
                {
                    return myModel;
                }
                Sentence clause = clauses[random.Next(clauses.Count)];

                IList<Symbol> symbolsInClause = sc.GetSymbolsIn(clause).ToList();
                
                if (random.NextDouble() >= probabilityOfRandomWalk)
                {
                    Symbol randomSymbol = symbolsInClause[random.Next(symbolsInClause.Count)];
                    myModel = myModel.Flip(randomSymbol);
                }
                else
                {
                    Symbol symbolToFlip = this.GetSymbolWhoseFlipMaximisesSatisfiedClauses(
                            new Converter<Sentence>().ListToSet(clauses),
                            symbolsInClause, myModel);
                    myModel = myModel.Flip(symbolToFlip);
                }

            }
            return null;
        }

        private Symbol GetSymbolWhoseFlipMaximisesSatisfiedClauses(
                ISet<Sentence> clauses, IList<Symbol> symbols, Model model)
        {
            if (symbols.Count > 0)
            {
                Symbol retVal = symbols[0];
                int maxClausesSatisfied = 0;
                foreach (Symbol sym in
                    symbols.Where(sym => this.GetNumberOfClausesSatisfiedIn(clauses, model.Flip(sym)) > maxClausesSatisfied))
                {
                    retVal = sym;
                    maxClausesSatisfied = this.GetNumberOfClausesSatisfiedIn(
                        clauses, model.Flip(sym));
                }
                return retVal;
            }
            return null;
        }

        private int GetNumberOfClausesSatisfiedIn(ISet<Sentence> clauses, Model model)
        {
            int retVal = 0;
            foreach(var s in clauses)
            {
                if (model.IsTrue(s))
                {
                    retVal += 1;
                }
            }
            return retVal;
        }
    }
}
